es{-}dds(${\it es}$;$i$;${\it ds}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}all(Id; id{-}deq; ${\it ds}$; $x$,$T$.es{-}dtype(${\it es}$; $i$; $x$; $T$))